Solving MaxSAT by Successive Calls to a SAT Solver

摘要

The Maximum Satisfiability (MaxSAT) problem is the problem of finding a truthassignment that maximizes the number of satisfied clauses of a given Booleanformula in Conjunctive Normal Form (CNF). Many exact solvers for MaxSAT havebeen developed during recent years, and many of them were presented in thewell-known SAT conference. Algorithms for MaxSAT generally fall into twocategories: (1) branch and bound algorithms and (2) algorithms that usesuccessive calls to a SAT solver (SAT- based), which this paper in on. Inpractical problems, SAT-based algorithms have been shown to be more efficient.This paper provides an experimental investigation to compare the performance ofrecent SAT-based and branch and bound algorithms on the benchmarks of theMaxSAT Evaluations.